| Definitions | es-E(es), es-pred?(es), p-graph(A; f), f(a), SWellFounded(R(x;y)), Unit, t  T, void, isect(A; x.B(x)), top, x:A  B(x),  x:A. B(x), subtype(S; T), Type, left + right, suptype(S; T), P   Q, final-iterate(f; x), es-init(es;e), event_system{i:l}, x:A  B(x), P  Q, rel_implies(T; R1; R2),   x,y. t(x;y), es-locl(es; e; e'), x.A(x), x. t(x), do-apply(f; x), s = t, can-apply(f; x),  b, A c B, prop{i:l}, x f y, Id, es-causl(es; e; e'), t.1, a < b, if b then t else f fi , False,  A, es-first(es; e), P  Q, sqequal(s; t), guard(T), sq_type(T), let x,y = A in B(x;y) |